% =====================================================================
% HOL Manual LaTeX Source: tutorial
% =====================================================================

\documentclass[12pt,fleqn]{book}
\usepackage{amsfonts}
\usepackage{alltt}
\usepackage{../LaTeX/layout}
\usepackage{graphicx}
\usepackage[hidelinks,hypertexnames=false,pdftitle={The HOL System TUTORIAL}]{hyperref}
%HEVEA \usepackage{epsfig}

\renewcommand\leadsto\rightarrow

% ---------------------------------------------------------------------
% Input defined macros and commands
% ---------------------------------------------------------------------
\input{../LaTeX/commands}
\input{../LaTeX/pic-macros}
%\input{../LaTeX/docmacros}
\usepackage{url}
\usepackage[line,arrow,frame,matrix]{xy}
\usepackage{tikz}
\usetikzlibrary{arrows,positioning}
\usepackage{../LaTeX/proof}
%\includeonly{title,contents,preface,../LaTeX/ack,intro,ml,logic,
% proof,references,Studies/preface,Studies/parity/parity}
%             Studies/microprocessor/all,
%\includeonly{Studies/microprocessor/all}
%\includeonly{Studies/int_mod/mod_arith_study/tutorial}
%\includeonly{binomial}
%\includeonly{parity}
\usepackage[strings]{underscore}


\begin{document}

   \setlength{\unitlength}{1mm}           % unit of length = 1mm
   \setlength{\baselineskip}{16pt}        % line spacing = 16pt

   % ---------------------------------------------------------------------
   % prelims
   % ---------------------------------------------------------------------

%   \pagenumbering{roman}                  % roman page numbers for prelims
%   \setcounter{page}{1}                   % start at page 1

   \include{title}                        % tutorial title page
   \include{preface}                      % preface to entire tutorial
   \input{../LaTeX/ack}                 % global acknowledgements
   \tableofcontents

%   \newpage
%   \pagenumbering{arabic}                % arabic page numbers
%   \setcounter{page}{1}                  % start at page 1

   \include{intro}                       % intro: getting and installing hol
   \include{ml}                          % intro to ml
   \include{writinghol}
%   \include{logic}                       % the HOL logic and intro to HOL proof
   \include{euclid}                      % Euclid example
   \include{parity}                      % parity example
%   \include{tool}                        % conjunction canonicalization tool
%   \include{binomial}                    % Andy Gordon's Binomial Thm in HOL
   \include{combin}                      % Combinatory logic
%   \include{conv}                        % Conversions
   \include{proof-tools}                 % Write your own DPLL Sat prover
   \include{more-examples}               % description of what's in examples/
   \include{references}                  % references

\end{document}
